\section{Vehicle/EngineSpeedSensor Classes}
\label{Section:SpeedSensors}
The \emph{VehicleSpeedSensor} is formalized thanks to the code reported in Listing~\ref{Code:VehicleSpeedSensor} while the \emph{EngineSpeedSensor} is formalized thanks to the code reported in Listing~\ref{Code:EngineSpeedSensor}.

During the formalization of sensors we decided to simplify the design assuming that every time a \texttt{sampleSpeed} event occurs the state variable \texttt{actualSpeed} - which is \texttt{time dependent} and \texttt{total} - is automatically updated with the actual measured speed. This means we don't provide any axioms formalizing this behavior.

Moreover, we specified the starting point of the constant frequency sample chain saying that sometimes in the past there was a \texttt{sampleSpeed} occurrence. Further more, we guarantee that \texttt{sampleSpeed} events will occur at constant frequency. In addition, if the sensor has memory we imposed that the \texttt{storedValue} is equal to 0. These can be consider just like the ``initial conditions'' of the system.

At the end, we guaranteed a sensor performs the needed action if and only if a sample event occur.

We didn't write any axioms specifying the fact that a \texttt{sendSpeed} event is mutually exclusive with itself due to the \texttt{total time dependent} parameter it accepts.

\lstinputlisting[language=TRIO,tabsize=4,numbers=left,numberstyle=\small,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=VehicleSpeedSensor.trio,label=Code:VehicleSpeedSensor]{../trio/VehicleSpeedSensor.trio}

\lstinputlisting[language=TRIO,tabsize=4,numbers=left,numberstyle=\small,basicstyle=\small,breaklines,breakatwhitespace,frame=single,caption=EngineSpeedSensor.trio,label=Code:EngineSpeedSensor]{../trio/EngineSpeedSensor.trio}
